
% \pagebreak[4]

% \hspace*{1cm}

% \pagebreak[4]

% \hspace*{1cm}

% \pagebreak[4]



\chapter{Цели и постановка задачи}

\ifpdf
    \graphicspath{{Chapter1/Chapter1Figs/PNG/}{Chapter1/Chapter1Figs/PDF/}{Chapter1/Chapter1Figs/}}
\else
    \graphicspath{{Chapter1/Chapter1Figs/EPS/}{Chapter1/Chapter1Figs/}}
\fi

\def\baselinestretch{1.5}

\section{Проблематика}

В разделе 1.3 было введено понятие нумералов Черча: \\
0 = $\lambda$s z. z \\
1 = $\lambda$ s z. s z \\
2 = $\lambda$ s z. s (s z) \\
3 = $\lambda$ s z. s (s (s z)) \\
4 = $\lambda$ s z. s (s (s (s z)))\\
 ... \\
Так же был изложена идея приписывания типа к 0. Применим аналогичные идеи для других нумералов Черча, в результате получим:\\
0: $\alpha$ $\to$ $\beta$ $\to$ $\beta$ \\
1: ($\beta$ $\to$ $\gamma$) $\to$ $\beta$ $\to$ $\gamma$ \\
2: ($\beta$ $\to$ $\beta$) $\to$ $\beta$ $\to$ $\beta$ \\
.. \\

n: ($\beta$ $\to$ $\beta$) $\to$ $\beta$ $\to$ $\beta$ \\
Затем запишем разность между 2 нумералами, к примеру: \\
5 - 4 = 1, 3 - 3 = 0\\

\hspace*{\fill} \\
С одной стороны ясно что тип результата должен быть в первом случае:\\
\begin{center}
($\beta$ $\to$ $\gamma$) $\to$ $\beta$ $\to$ $\gamma$
\end{center}
, а во втором
\begin{center}
($\beta$ $\to$ $\beta$) $\to$ $\beta$ $\to$ $\beta$ \\
\end{center}

Но с другой стороны, мы знаем что \\
\begin{center}
0: $\alpha$ $\to$ $\beta$ $\to$ $\beta$ \\
1: ($\beta$ $\to$ $\gamma$) $\to$ $\beta$ $\to$ $\gamma$ \\
\end{center}

Этот пример продемонстрировал интересный эффект: при некоторых экспансиях в нумералах Черча происходит изменение наиболее общего типа. \\
\section{Цели и задачи}
Сформулируем цель и задачи данной работы. \\
Итак в предыдущем пункте мы привели пример изменения наиболее общего типа при экспансии. Как обобщение примера, целью данной работы является исследование эффекта изменения типа при экспансии. Для решения данной задачи разобьем ей на подзадачи. \\

\begin{itemize}
  \item Реализовать систему пошаговой редукции.
  \item Реализовать систему вывода типов.
  \item Определить условия, при которых имеет место эффект изменения типа.
\end{itemize}
Помимо этого, необходимо реализовать библиотеку комбинаторов, которая позволит быстро искать необходимый эффект.

%: ----------------------- HELP: latex document organisation

% the commands below help you to subdivide and organise your thesis

%    \chapter{}       = level 1, top level

%    \section{}       = level 2

%    \subsection{}    = level 3

%    \subsubsection{} = level 4

% note that everything after the percentage sign is hidden from output















%%% Local Variables: 

%%% mode: latex

%%% TeX-master: "../thesis"

%%% End: 


